(set-option :produce-interpolants 1)
(set-option :proof-reduce 1)
;(set-option :proof-check 1)
;(set-option :verbosity 2)
(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun f () Bool)

(assert (!(not a) :named A))
(assert (!(and (or a (or a b)) (and (not c) (or e (or a b))))
    :named B))

(assert (!(and
    (or a d e)
    (or a (not d) e)
    (or a d f)
    (or a (not d) f)
    (or a (not e) (not f) (not b) c)
 )
:named C))
(check-sat)
(get-interpolants A B C)
